package wenjiesha.victor.gmail.com;

/* class Global Calculus
 * an abbreviated Global Calculus
 * no data transmission is included
 * syntax:
 * 	I ::= A->B:ch(s).I
 *       |A->B:s<op>.I
 *       |I1+I2
 *       |I1|I2
 *       |XA
 *       |rec XA.I
 *       |0
 *  
 * Reduction Rules:
 *  rule 0: (M, A->B:ch(s).I)B -> (M start, I)B  
 *  rule 1: (M, A->B:s<op>.I)B -> (M add token, I)B
 *  rule 2: if rule 3 stands (M, B->A:s<op>.I)B -> (M remove token, I)B
 *  rule 3: if(B has token in corresponding communication place)
 *  
 *  rule 4: (M, I1+I2) -> (M', Ii')
 *  rule 5: if(M, I1) -> (M', I1'), then (M, I1|I2) -> (M', I1'|I2)
 *  rule 6: if(M, I[recXA.I/XA]) -> (M', I'), then (M, recXA.I) -> (M', I')
 *  
 *  Structural Equality
 *  I+I == I
 *  I|0 == I
 *  I1|I2 == I2|I1
 *  I1+I2 == I2+I1
 * 	
 * */
public class GlobalCalculus {
	
		
}


